Termination w.r.t. Q proof of TRS/TRCSREx7_BLR02

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__from(X)) → FROM(activate(X))
TAKE(s(N), cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__s(X)) → S(activate(X))
SEL(s(N), cons(X, XS)) → ACTIVATE(XS)
SEL(s(N), cons(X, XS)) → SEL(N, activate(XS))
2ND(cons(X, XS)) → HEAD(activate(XS))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
2ND(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__from(X)) → FROM(activate(X))
TAKE(s(N), cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__s(X)) → S(activate(X))
SEL(s(N), cons(X, XS)) → ACTIVATE(XS)
SEL(s(N), cons(X, XS)) → SEL(N, activate(XS))
2ND(cons(X, XS)) → HEAD(activate(XS))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
2ND(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TAKE(s(N), cons(X, XS)) → ACTIVATE(XS)
2ND(cons(X, XS)) → HEAD(activate(XS))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__from(X)) → FROM(activate(X))
SEL(s(N), cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__s(X)) → S(activate(X))
SEL(s(N), cons(X, XS)) → SEL(N, activate(XS))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
2ND(cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 5 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TAKE(s(N), cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)

The remaining pairs can at least be oriented weakly.

TAKE(s(N), cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)

Used ordering: Combined order from the following AFS and order.
TAKE(x1, x2) = TAKE(x2)
s(x1) = x1
cons(x1, x2) = x2
ACTIVATE(x1) = ACTIVATE(x1)
n__take(x1, x2) = n__take(x1, x2)
n__from(x1) = x1
activate(x1) = x1
n__s(x1) = x1
take(x1, x2) = take(x1, x2)
from(x1) = x1
0 = 0
nil = nil

Lexicographic path order with status [19].
Quasi-Precedence:

[TAKE₁, ACTIVATE_1] > nil
[n_{_take₂}, take_2] > nil
0 > nil

Status:

ACTIVATE₁: [1]
TAKE₁: [1]
0: multiset
nil: multiset
take₂: [1,2]
n_{_take₂}: [1,2]

The following usable rules [14] were oriented:

take(X1, X2) → n__take(X1, X2)
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
from(X) → n__from(X)
activate(n__s(X)) → s(activate(X))
activate(X) → X
take(0, XS) → nil
from(X) → cons(X, n__from(n__s(X)))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
s(X) → n__s(X)
activate(n__from(X)) → from(activate(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TAKE(s(N), cons(X, XS)) → ACTIVATE(XS)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__from(X)) → ACTIVATE(X)

The remaining pairs can at least be oriented weakly.

ACTIVATE(n__s(X)) → ACTIVATE(X)

Used ordering: Combined order from the following AFS and order.
ACTIVATE(x1) = ACTIVATE(x1)
n__from(x1) = n__from(x1)
n__s(x1) = x1

Lexicographic path order with status [19].
Quasi-Precedence:

[ACTIVATE₁, n_{_{from_1]}}

Status:

ACTIVATE₁: [1]
n_{_from₁}: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__s(X)) → ACTIVATE(X)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
ACTIVATE(x1) = ACTIVATE(x1)
n__s(x1) = n__s(x1)

Lexicographic path order with status [19].
Quasi-Precedence:

[ACTIVATE₁, n_{_{s_1]}}

Status:

ACTIVATE₁: [1]
n_{_s₁}: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ PisEmptyProof

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

SEL(s(N), cons(X, XS)) → SEL(N, activate(XS))

The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SEL(s(N), cons(X, XS)) → SEL(N, activate(XS))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SEL(x1, x2) = x1
s(x1) = s(x1)
cons(x1, x2) = cons(x1, x2)
activate(x1) = activate(x1)
take(x1, x2) = take(x1, x2)
n__take(x1, x2) = n__take
from(x1) = x1
n__from(x1) = x1
n__s(x1) = n__s(x1)
0 = 0
nil = nil

Lexicographic path order with status [19].
Quasi-Precedence:

n_{_s₁} > [s₁, cons₂, activate₁, take₂, n_{_take]}

Status:

n_{_take}: []
n_{_s₁}: [1]
0: multiset
s₁: [1]
nil: multiset
cons₂: [1,2]
take₂: [2,1]
activate₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

from(X) → cons(X, n__from(n__s(X)))
head(cons(X, XS)) → X
2nd(cons(X, XS)) → head(activate(XS))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, activate(XS))
from(X) → n__from(X)
s(X) → n__s(X)
take(X1, X2) → n__take(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.